PRISM
=====
Version: 4.5.dev
Date: Sat Apr 03 05:38:25 CEST 2021
Hostname: christopher
Memory limits: cudd=4g, java(heap)=11g
Command line: prism -javamaxmem 11g -cuddmaxmem 4g -heuristic speed -e 1e-6 -maxiters 1000000 ij.60.prism ij.60.props --property stable
Parsing model file "ij.60.prism"...
Type: MDP
Modules: process0 process1 process2 process3 process4 process5 process6 process7 process8 process9 process10 process11 process12 process13 process14 process15 process16 process17 process18 process19 process20 process21 process22 process23 process24 process25 process26 process27 process28 process29 process30 process31 process32 process33 process34 process35 process36 process37 process38 process39 process40 process41 process42 process43 process44 process45 process46 process47 process48 process49 process50 process51 process52 process53 process54 process55 process56 process57 process58 process59
Variables: q0 q1 q2 q3 q4 q5 q6 q7 q8 q9 q10 q11 q12 q13 q14 q15 q16 q17 q18 q19 q20 q21 q22 q23 q24 q25 q26 q27 q28 q29 q30 q31 q32 q33 q34 q35 q36 q37 q38 q39 q40 q41 q42 q43 q44 q45 q46 q47 q48 q49 q50 q51 q52 q53 q54 q55 q56 q57 q58 q59 num_tokens_var
Parsing properties file "ij.60.props"...
1 property:
(1) "stable": Pmax=? [ F ((q0+q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18+q19+q20+q21+q22+q23+q24+q25+q26+q27+q28+q29+q30+q31+q32+q33+q34+q35+q36+q37+q38+q39+q40+q41+q42+q43+q44+q45+q46+q47+q48+q49+q50+q51+q52+q53+q54+q55+q56+q57+q58+q59)=1) ]
---------------------------------------------------------------------
Model checking: "stable": Pmax=? [ F ((q0+q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18+q19+q20+q21+q22+q23+q24+q25+q26+q27+q28+q29+q30+q31+q32+q33+q34+q35+q36+q37+q38+q39+q40+q41+q42+q43+q44+q45+q46+q47+q48+q49+q50+q51+q52+q53+q54+q55+q56+q57+q58+q59)=1) ]
Warning: Switching to sparse engine and (backwards) Gauss Seidel (default for heuristic=speed).
Building model...
Computing reachable states...
Reachability (BFS): 60 iterations in 0.04 seconds (average 0.000717, setup 0.00)
Time for model construction: 0.183 seconds.
Type: MDP
States: 1152921504606846976 (1 initial)
Transitions: 6.052837899185947E19
Choices: 3.458764513820541E19
Transition matrix: 8493 nodes (3 terminal), 6.052837899185947E19 minterms, vars: 66r/66c/59nd
Warning: Switching to MTBDD engine, as number of states is too large for Sparse engine.
Prob0A: 60 iterations in 7.52 seconds (average 0.125400, setup 0.00)
Prob1E: 61 iterations in 8.20 seconds (average 0.134393, setup 0.00)
yes = 1152921504606846976, no = 0, maybe = 0
Value in the initial state: 1.0
Time for model checking: 15.819 seconds.
Result: 1.0 (value in the initial state)
Overall running time: 16.256 seconds.
---------------------------------------------------------------------
Note: There were 2 warnings during computation.